A:Type, x:A. (x,y:A. decidable((x = y)))  (L:(A List). decidable((x  L))) 

latex

Definitions	x:A. B(x), P  Q, prop{i:l}, t  T, P  Q, P  Q, P  Q, P  Q
Lemmas	decidable functionality, l member wf, false wf, nil member, decidable false, cons member, decidable or, decidable wf